(0) Obligation:
Clauses:
div(0, Y, 0) :- no(zero(Y)).
div(X, Y, s(Z)) :- ','(no(zero(X)), ','(no(zero(Y)), ','(minus(X, Y, U), div(U, Y, Z)))).
minus(0, Y, 0).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X1).
failure(b).
Query: div(g,g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
minusC(s(X1), s(X2), X3) :- minusC(X1, X2, X3).
divA(s(X1), s(X2), s(X3)) :- minusC(X1, X2, X4).
divA(X1, X2, s(X3)) :- ','(minuscB(X1, X2, X4), divA(X4, X2, X3)).
Clauses:
divcA(0, X1, 0).
divcA(X1, X2, s(X3)) :- ','(minuscB(X1, X2, X4), divcA(X4, X2, X3)).
minuscC(0, X1, 0).
minuscC(X1, 0, X1).
minuscC(s(X1), s(X2), X3) :- minuscC(X1, X2, X3).
minuscB(s(X1), s(X2), X3) :- minuscC(X1, X2, X3).
Afs:
divA(x1, x2, x3) = divA(x1, x2)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
divA_in: (b,b,f)
minusC_in: (b,b,f)
minuscB_in: (b,b,f)
minuscC_in: (b,b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
DIVA_IN_GGA(s(X1), s(X2), s(X3)) → U2_GGA(X1, X2, X3, minusC_in_gga(X1, X2, X4))
DIVA_IN_GGA(s(X1), s(X2), s(X3)) → MINUSC_IN_GGA(X1, X2, X4)
MINUSC_IN_GGA(s(X1), s(X2), X3) → U1_GGA(X1, X2, X3, minusC_in_gga(X1, X2, X3))
MINUSC_IN_GGA(s(X1), s(X2), X3) → MINUSC_IN_GGA(X1, X2, X3)
DIVA_IN_GGA(X1, X2, s(X3)) → U3_GGA(X1, X2, X3, minuscB_in_gga(X1, X2, X4))
U3_GGA(X1, X2, X3, minuscB_out_gga(X1, X2, X4)) → U4_GGA(X1, X2, X3, divA_in_gga(X4, X2, X3))
U3_GGA(X1, X2, X3, minuscB_out_gga(X1, X2, X4)) → DIVA_IN_GGA(X4, X2, X3)
The TRS R consists of the following rules:
minuscB_in_gga(s(X1), s(X2), X3) → U9_gga(X1, X2, X3, minuscC_in_gga(X1, X2, X3))
minuscC_in_gga(0, X1, 0) → minuscC_out_gga(0, X1, 0)
minuscC_in_gga(X1, 0, X1) → minuscC_out_gga(X1, 0, X1)
minuscC_in_gga(s(X1), s(X2), X3) → U8_gga(X1, X2, X3, minuscC_in_gga(X1, X2, X3))
U8_gga(X1, X2, X3, minuscC_out_gga(X1, X2, X3)) → minuscC_out_gga(s(X1), s(X2), X3)
U9_gga(X1, X2, X3, minuscC_out_gga(X1, X2, X3)) → minuscB_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
divA_in_gga(
x1,
x2,
x3) =
divA_in_gga(
x1,
x2)
s(
x1) =
s(
x1)
minusC_in_gga(
x1,
x2,
x3) =
minusC_in_gga(
x1,
x2)
minuscB_in_gga(
x1,
x2,
x3) =
minuscB_in_gga(
x1,
x2)
U9_gga(
x1,
x2,
x3,
x4) =
U9_gga(
x1,
x2,
x4)
minuscC_in_gga(
x1,
x2,
x3) =
minuscC_in_gga(
x1,
x2)
0 =
0
minuscC_out_gga(
x1,
x2,
x3) =
minuscC_out_gga(
x1,
x2,
x3)
U8_gga(
x1,
x2,
x3,
x4) =
U8_gga(
x1,
x2,
x4)
minuscB_out_gga(
x1,
x2,
x3) =
minuscB_out_gga(
x1,
x2,
x3)
DIVA_IN_GGA(
x1,
x2,
x3) =
DIVA_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
MINUSC_IN_GGA(
x1,
x2,
x3) =
MINUSC_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIVA_IN_GGA(s(X1), s(X2), s(X3)) → U2_GGA(X1, X2, X3, minusC_in_gga(X1, X2, X4))
DIVA_IN_GGA(s(X1), s(X2), s(X3)) → MINUSC_IN_GGA(X1, X2, X4)
MINUSC_IN_GGA(s(X1), s(X2), X3) → U1_GGA(X1, X2, X3, minusC_in_gga(X1, X2, X3))
MINUSC_IN_GGA(s(X1), s(X2), X3) → MINUSC_IN_GGA(X1, X2, X3)
DIVA_IN_GGA(X1, X2, s(X3)) → U3_GGA(X1, X2, X3, minuscB_in_gga(X1, X2, X4))
U3_GGA(X1, X2, X3, minuscB_out_gga(X1, X2, X4)) → U4_GGA(X1, X2, X3, divA_in_gga(X4, X2, X3))
U3_GGA(X1, X2, X3, minuscB_out_gga(X1, X2, X4)) → DIVA_IN_GGA(X4, X2, X3)
The TRS R consists of the following rules:
minuscB_in_gga(s(X1), s(X2), X3) → U9_gga(X1, X2, X3, minuscC_in_gga(X1, X2, X3))
minuscC_in_gga(0, X1, 0) → minuscC_out_gga(0, X1, 0)
minuscC_in_gga(X1, 0, X1) → minuscC_out_gga(X1, 0, X1)
minuscC_in_gga(s(X1), s(X2), X3) → U8_gga(X1, X2, X3, minuscC_in_gga(X1, X2, X3))
U8_gga(X1, X2, X3, minuscC_out_gga(X1, X2, X3)) → minuscC_out_gga(s(X1), s(X2), X3)
U9_gga(X1, X2, X3, minuscC_out_gga(X1, X2, X3)) → minuscB_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
divA_in_gga(
x1,
x2,
x3) =
divA_in_gga(
x1,
x2)
s(
x1) =
s(
x1)
minusC_in_gga(
x1,
x2,
x3) =
minusC_in_gga(
x1,
x2)
minuscB_in_gga(
x1,
x2,
x3) =
minuscB_in_gga(
x1,
x2)
U9_gga(
x1,
x2,
x3,
x4) =
U9_gga(
x1,
x2,
x4)
minuscC_in_gga(
x1,
x2,
x3) =
minuscC_in_gga(
x1,
x2)
0 =
0
minuscC_out_gga(
x1,
x2,
x3) =
minuscC_out_gga(
x1,
x2,
x3)
U8_gga(
x1,
x2,
x3,
x4) =
U8_gga(
x1,
x2,
x4)
minuscB_out_gga(
x1,
x2,
x3) =
minuscB_out_gga(
x1,
x2,
x3)
DIVA_IN_GGA(
x1,
x2,
x3) =
DIVA_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
MINUSC_IN_GGA(
x1,
x2,
x3) =
MINUSC_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MINUSC_IN_GGA(s(X1), s(X2), X3) → MINUSC_IN_GGA(X1, X2, X3)
The TRS R consists of the following rules:
minuscB_in_gga(s(X1), s(X2), X3) → U9_gga(X1, X2, X3, minuscC_in_gga(X1, X2, X3))
minuscC_in_gga(0, X1, 0) → minuscC_out_gga(0, X1, 0)
minuscC_in_gga(X1, 0, X1) → minuscC_out_gga(X1, 0, X1)
minuscC_in_gga(s(X1), s(X2), X3) → U8_gga(X1, X2, X3, minuscC_in_gga(X1, X2, X3))
U8_gga(X1, X2, X3, minuscC_out_gga(X1, X2, X3)) → minuscC_out_gga(s(X1), s(X2), X3)
U9_gga(X1, X2, X3, minuscC_out_gga(X1, X2, X3)) → minuscB_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
minuscB_in_gga(
x1,
x2,
x3) =
minuscB_in_gga(
x1,
x2)
U9_gga(
x1,
x2,
x3,
x4) =
U9_gga(
x1,
x2,
x4)
minuscC_in_gga(
x1,
x2,
x3) =
minuscC_in_gga(
x1,
x2)
0 =
0
minuscC_out_gga(
x1,
x2,
x3) =
minuscC_out_gga(
x1,
x2,
x3)
U8_gga(
x1,
x2,
x3,
x4) =
U8_gga(
x1,
x2,
x4)
minuscB_out_gga(
x1,
x2,
x3) =
minuscB_out_gga(
x1,
x2,
x3)
MINUSC_IN_GGA(
x1,
x2,
x3) =
MINUSC_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MINUSC_IN_GGA(s(X1), s(X2), X3) → MINUSC_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
MINUSC_IN_GGA(
x1,
x2,
x3) =
MINUSC_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUSC_IN_GGA(s(X1), s(X2)) → MINUSC_IN_GGA(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MINUSC_IN_GGA(s(X1), s(X2)) → MINUSC_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIVA_IN_GGA(X1, X2, s(X3)) → U3_GGA(X1, X2, X3, minuscB_in_gga(X1, X2, X4))
U3_GGA(X1, X2, X3, minuscB_out_gga(X1, X2, X4)) → DIVA_IN_GGA(X4, X2, X3)
The TRS R consists of the following rules:
minuscB_in_gga(s(X1), s(X2), X3) → U9_gga(X1, X2, X3, minuscC_in_gga(X1, X2, X3))
minuscC_in_gga(0, X1, 0) → minuscC_out_gga(0, X1, 0)
minuscC_in_gga(X1, 0, X1) → minuscC_out_gga(X1, 0, X1)
minuscC_in_gga(s(X1), s(X2), X3) → U8_gga(X1, X2, X3, minuscC_in_gga(X1, X2, X3))
U8_gga(X1, X2, X3, minuscC_out_gga(X1, X2, X3)) → minuscC_out_gga(s(X1), s(X2), X3)
U9_gga(X1, X2, X3, minuscC_out_gga(X1, X2, X3)) → minuscB_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
minuscB_in_gga(
x1,
x2,
x3) =
minuscB_in_gga(
x1,
x2)
U9_gga(
x1,
x2,
x3,
x4) =
U9_gga(
x1,
x2,
x4)
minuscC_in_gga(
x1,
x2,
x3) =
minuscC_in_gga(
x1,
x2)
0 =
0
minuscC_out_gga(
x1,
x2,
x3) =
minuscC_out_gga(
x1,
x2,
x3)
U8_gga(
x1,
x2,
x3,
x4) =
U8_gga(
x1,
x2,
x4)
minuscB_out_gga(
x1,
x2,
x3) =
minuscB_out_gga(
x1,
x2,
x3)
DIVA_IN_GGA(
x1,
x2,
x3) =
DIVA_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIVA_IN_GGA(X1, X2) → U3_GGA(X1, X2, minuscB_in_gga(X1, X2))
U3_GGA(X1, X2, minuscB_out_gga(X1, X2, X4)) → DIVA_IN_GGA(X4, X2)
The TRS R consists of the following rules:
minuscB_in_gga(s(X1), s(X2)) → U9_gga(X1, X2, minuscC_in_gga(X1, X2))
minuscC_in_gga(0, X1) → minuscC_out_gga(0, X1, 0)
minuscC_in_gga(X1, 0) → minuscC_out_gga(X1, 0, X1)
minuscC_in_gga(s(X1), s(X2)) → U8_gga(X1, X2, minuscC_in_gga(X1, X2))
U8_gga(X1, X2, minuscC_out_gga(X1, X2, X3)) → minuscC_out_gga(s(X1), s(X2), X3)
U9_gga(X1, X2, minuscC_out_gga(X1, X2, X3)) → minuscB_out_gga(s(X1), s(X2), X3)
The set Q consists of the following terms:
minuscB_in_gga(x0, x1)
minuscC_in_gga(x0, x1)
U8_gga(x0, x1, x2)
U9_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(17) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
U3_GGA(X1, X2, minuscB_out_gga(X1, X2, X4)) → DIVA_IN_GGA(X4, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(DIVA_IN_GGA(x1, x2)) = 1 + x1
POL(U3_GGA(x1, x2, x3)) = 1 + x3
POL(U8_gga(x1, x2, x3)) = 1 + x3
POL(U9_gga(x1, x2, x3)) = 1 + x3
POL(minuscB_in_gga(x1, x2)) = x1
POL(minuscB_out_gga(x1, x2, x3)) = 1 + x3
POL(minuscC_in_gga(x1, x2)) = x1
POL(minuscC_out_gga(x1, x2, x3)) = x3
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
minuscB_in_gga(s(X1), s(X2)) → U9_gga(X1, X2, minuscC_in_gga(X1, X2))
minuscC_in_gga(0, X1) → minuscC_out_gga(0, X1, 0)
minuscC_in_gga(X1, 0) → minuscC_out_gga(X1, 0, X1)
minuscC_in_gga(s(X1), s(X2)) → U8_gga(X1, X2, minuscC_in_gga(X1, X2))
U9_gga(X1, X2, minuscC_out_gga(X1, X2, X3)) → minuscB_out_gga(s(X1), s(X2), X3)
U8_gga(X1, X2, minuscC_out_gga(X1, X2, X3)) → minuscC_out_gga(s(X1), s(X2), X3)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIVA_IN_GGA(X1, X2) → U3_GGA(X1, X2, minuscB_in_gga(X1, X2))
The TRS R consists of the following rules:
minuscB_in_gga(s(X1), s(X2)) → U9_gga(X1, X2, minuscC_in_gga(X1, X2))
minuscC_in_gga(0, X1) → minuscC_out_gga(0, X1, 0)
minuscC_in_gga(X1, 0) → minuscC_out_gga(X1, 0, X1)
minuscC_in_gga(s(X1), s(X2)) → U8_gga(X1, X2, minuscC_in_gga(X1, X2))
U8_gga(X1, X2, minuscC_out_gga(X1, X2, X3)) → minuscC_out_gga(s(X1), s(X2), X3)
U9_gga(X1, X2, minuscC_out_gga(X1, X2, X3)) → minuscB_out_gga(s(X1), s(X2), X3)
The set Q consists of the following terms:
minuscB_in_gga(x0, x1)
minuscC_in_gga(x0, x1)
U8_gga(x0, x1, x2)
U9_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(19) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(20) TRUE